package server.sat;

import java.sql.Connection;
import java.sql.PreparedStatement;
import java.sql.SQLException;
import java.sql.Statement;
import java.util.concurrent.Callable;

import javax.sql.rowset.serial.SerialBlob;

import server.core.Database;
import server.core.Problem;
import server.core.ProblemManager;
import server.core.Solution;

/**
 * The SATProblemManager class defines the implementation of the
 * {@link ProblemManager} interface for SAT.
 * 
 * @author Clayton Edward Taylor
 */
public class SATProblemManager implements ProblemManager {
	
	private Database db;
	
	/**
	 * Creates a new SATProblemManager and sets up a table in the 
	 * {@link Database} to act as the cache for it.
	 * 
	 * @param db - The Database to use as a cache
	 * @throws     SQLException If the creation of the table fails
	 * @see        SATProblemManager
	 */
	public SATProblemManager(Database db) throws SQLException {
		
		this.db = db;
		Connection c = db.getConnection();
		Statement st = c.createStatement();
		String sql = "CREATE TABLE IF NOT EXISTS `sat_cache`"
				+ " ( `problem_key` CHAR(64), "
				+ " UNIQUE KEY ( `problem_key` ), "
				+ " `search_count` INTEGER,"
				+ " `num_vars` INTEGER,"
				+ " `solution` BLOB )";
		try {
			st.execute(sql);
		} finally {
			st.close();
		}
	}
	
	/**
	 * Creates a new {@link SATProblemParser} object for the given data and
	 * returns it.
	 * 
	 * @param data - The CNF data to parse
	 * @return       A SATProblemParser object
	 * @see          SATProblemManager
	 */
	@Override
	public Callable<Problem> getProblemParser(String data) {
		
		return new SATProblemParser(data);
	}
	
	/**
	 * Creates a new {@link SATCacheQuery} object for the given 
	 * {@link SATProblem} and returns it.
	 * 
	 * @param p - The SATProblem object
	 * @return    A SATCacheQuery object
	 * @see       SATProblemManager
	 */
	@Override
	public Callable<Solution> getCacheQuery(Problem p) {
		
		return new SATCacheQuery(db, ((SATProblem) p).getKey());
	}

	/**
	 * Creates a new {@link SATSolverDispatch} object for the given 
	 * {@link SATProblem} and returns it.
	 * 
	 * @param p - The SATProblem object
	 * @return    A SATSolverDispatch object
	 * @see       SATProblemManager
	 */
	@Override
	public Callable<Solution> getSolverDispatch(Problem p) {
		
		return new SATSolverDispatch(((SATProblem) p).getData());
	}
	
	/**
	 * Inserts the given {@link SATSolution} into the {@link Database}
	 * for the given {@link SATProblem}.
	 * 
	 * @param p - The SATProblem object
	 * @param s - The SATSolution object
	 * @see       SATProblemManager
	 */
	@Override
	public void insertCache(Problem p, Solution s) {
		
		String sql = "INSERT IGNORE INTO `sat_cache`"
				+ " ( `problem_key`, `search_count`, `num_vars`, `solution` )"
				+ " VALUES ( ?, ?, ?, ? )"
				+ " ON DUPLICATE KEY UPDATE"
				+ " `search_count` = `search_count` + 1";
		
		SATProblem sp = (SATProblem) p;
		SATSolution ss = (SATSolution) s;
		try {
			Connection c = db.getConnection();
			PreparedStatement ps = c.prepareStatement(sql);
			try {
				ps.setString(1, sp.getKey());
				ps.setInt(2, 1);
				ps.setInt(3, ss.getNumVariables());
				if (ss.getNumVariables() == 0) {
					ps.setNull(4, java.sql.Types.BLOB);
				} else {
					ps.setBlob(4, new SerialBlob(ss.getBytes()));
				}
				ps.executeUpdate();
			} catch (SQLException e) {
				return;
			} finally {
				ps.close();
			}
		} catch (SQLException e) {
			return;
		}
	}
	
	/**
	 * Clears out the cache for SAT.
	 * 
	 * @see SATProblemManager
	 */
	@Override
	public void clearCache() {
		
		String sql = "TRUNCATE TABLE `sat_cache`";
		try {
			Connection c = db.getConnection();
			Statement st = c.createStatement();
			try {
				st.execute(sql);
			} finally {
				st.close();
			}
		} catch (SQLException e) {
			return;
		}
	}
}
